Nuprl Lemma : l_contains_weakening
11,40
postcript
pdf
T
:Type,
A
,
B
:(
T
List). (
A
=
B
)
A
B
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
(
x
l
)
,
P
Q
,
x
L
.
P
(
x
)
,
A
B
,
Lemmas
l
contains
wf
,
l
member
wf
origin
T:Type, A, B:(T List). (A = B) 
A 
B T:Type, A, B:(T List). (A = B) A B 
Tx:A. B(x) l) QxL. P(x) B